A framework for proving correctness of adjoint message-passing programs

摘要

We propose a technique for proving correctness of adjoint message passing programs that relies on data dependences in partitioned global address space. As an example we discuss asynchronous unbuffered send/receive using MPI. ?? 2008 Springer-Verlag Berlin Heidelberg.